*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=

First reviewer's review:

Summary of the submission <<<

The paper presents a formal semantics for handling null values in the
evaluation of OCL expressions. This is done by incorporating null as a valid
operation argument and collection element, so that potentially null values can
be used in conjunction with otherwise strict OCL operations. In particular, the
paper discusses how having null values impacts manipulation of primitive data
types, class typing, accessor functions, multiplicity constraints, and some of
OCL's special functions (e.g. allInstances). As an example, the authors show
how their proposed semantics simplifies the specification of red-black trees in
OCL.

Evaluation <<<

The problem tackled by the paper is interesting. Indeed, the lack of proper
semantics for null (or any other special value, for that matter) can be a
hassle when writing logical expressions, as one has to keep track of operations
that might potentially be passed null values and write additional checks for
handling these values (this can cause unnecessary complexity). The paper also
presents a nice exercise in formalizing OCL semantics, building on the previous
work of the authors on the subject. 

Having said the above, I have doubts about the value of the paper. My main
concern is that very little conclusion can be drawn from the work in its
current stage. 

[I find the lack of consistency in your report quite embarassing. 
The paper provides a "nice exercise of an OCL" semantics resolving
an open problem, but no conclusions can be drawn from that ?

Moreover, we presented a collection of in parts formally proven 
properties over this semantics, which could be used in a new
mandatory part of a new standard document.

Or do you have a fundamental problem with the usual
scheme of a scientific paper: definitions - theorems ?
]

All that is provided towards illustration and validation of the
semantics is a very simple example (red-black trees). 

[We maintain that it is actually a quite complex problem,
using our experience in concrete program verification.]

Further, there is no
discussion of possible alternative semantics and limitations. 
[True, but this is practically impossible.]
Hence, it is unclear to me what the pros and cons of adopting the proposed semantics are.
[There is actually a current line of discussion for alternative
design choices on different topics such as: smashedness, 
non-null-types, changing the class hierarchy. This could
be strengthened, but only to a small extent.]

I also wonder if one can avoid a full revisit of the underlying semantics of
OCL every time a new logical value needs to be added. In fact, there has been a
lot of research on externalizing the logic of handling additional truth values
(e.g. unknown, uncertain, inapplicable, conflicting, etc). For example, see
[Chechik et al] where a multiple-valued semantics is defined for temporal
logics using lattices, [Woodcock] where a semantics for partiality in Z is
provided by augmenting classical logic with guards, and [Nentwitch et al] where
a hyperlinked-based semantics (as opposed to a Boolean semantics) is defined
for first-order logic to enable linking collections of inconsistent model
elements. It is interesting to see whether or not OCL can be augmented in
similar ways to decouple its core semantics from the semantics of the truth
values involved.

[This is a quite fantastic speculation, given that we are talking
on a concrete language and not on an artificial example in 
aspect-oriented language design.]

Detailed comments to the authors:
* Section 2.2 must move to an implementation section towards the end of the
paper.
* The opening to Section 4.2 is written poorly and is very difficult to follow.
I don't understand the first sentence ("Of course, it is a viable ..."). What
do you mean by a "discipline of constructors"? Also, the adverbs
"pragmatically", "technically", "methodologically", and "semantically" bear
little meaning and need to be dropped.
* It would be very helpful to provide a summary of the assumptions you made in
regards to issues such as dangling references, the framing problem,
interpretation of null in collections, etc. This can aid the reader in deciding
if your semantics are applicable in a certain context.

Minor comments:
* I don't understand what you mean by "textbook style". Is this supposed to
mean high-level?
* Page 4: "avoid to show" -> "do not show"
* Page 5: "The majority of the operations is strict"
                    ^^^ are
* Page 6: I[X->forall(x|P(x)] - there is a parenthesis missing.
* Page 7: incomplete sentence - "the reader interested in a complete model is
referred to ..."
* Page 8: We consider the case of an attribute a of class C"
                       ^^^^ of a
* Same page (just before 4.1): "In later versions of the standard ..." - I had
no idea what this sentence means.
* Page 9: "... case for collection types is analogously" - is "handled
analogously" or is "analogous".
* Page 10: "casted" -> "cast"

References:
[Chechik et al] Multi-valued symbolic model-checking
[Woodcock] The Verified Software Repository
[Nentwitch et al] xlinkit: a consistency checking and smart link generation
service

*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*

Second reviewer's review:

Summary of the submission <<<

The paper proposes a formal redefinition of OCL with a null value to
overcome the inconsistencies in the lastest OCL standard which include
this null value. This formal semantics is based on HOL-OCL, a
higher-order logic extension of OCL, with a supporting tool framework.

Evaluation <<<

Points in favour
- The topic of this paper, to clarify the semantics of OCL in the presence of 
null references and correct existing inconsistencies, is an important one 
and should be addressed
- The paper seems to be generally correct and is machine-checked
- There is tool support for HOL-OCL
- The example presented highlights the pragmatic implications of the new
semantics
- The paper is largely well written (save for a few issues, see below)

Points against
- The motivating example might not be convincing enough: The authors
argue that having a null reference simplifies modelling, because 
it obviates the need to model, e.g., empty trees explicitly. 
However, this "burden" can sometimes lead to cleaner designs. 
For instance, if I want to develop operations that work on trees, 
for example a pretty-printer, a natural choice of design pattern is 
the interpreter pattern or the visitor pattern, both of which rely on
the composite pattern, which assumes that all kinds of trees are
represented by their own classes; 

[Admittedly, the use of empty trees that you suggest has advantages. 
Note, however, that the resulting models have a different memory-
behaviour and are therefore not used in concrete implementations
in JAVA or C++. It was our explicit goal to show how OCL can be
changed to adress design level contracts. ]

providing a uniform interface for
each kind of tree, including the empty tree. We might want to have
the pretty-printer do something special with empty trees, and
therefore empty trees should be explicitly represented by their own
class. In other words, when using these common design patterns null
references seem to be less relevant, as you would end up modelling
the "empty" objects explicitly anyway.

Specific comments:
Section 2.2.
* In Figure 1, some of the arrows seem to have different meanings. For
example, the arrows going from SML to Isabelle/HOL and to su4sml seem
to represent the relation "is implemented in", but other arrows seem
to represent information flow. Perhaps different arrow styles would
make this clear.

Section 3.2.
* The semantics does not make entirely clear which is the semantic
domain of the interpretation function I[.]. It might be helpful to
say that if E is an expression of type \alpha then I[E] is of type
V(\alpha).
* semantic equation for "not X": on the right hand side, shouldn't it
say "if I[X]\tau" instead of "if [X]\tau"? 

Section 3.3.
* In the interpretation of forall, there is a right parenthesis missing 
in I[X->forall(x|P(x)].
* Also in the interpretation of forall, the role of \lambda \tau.x is
unclear. How do I interpret Y->forall(x|x.a=5)? It would depend on
I[P(\lambda \tau.x)]\tau where P(x) is x.a=5, but what is that? Is
P(\lambda \tau.x) = (\lambda \tau.x).a = 5? What does that mean?
Section 3.4. 
* "for this, that will" -> "for these concepts that will"
* "we will have to clarify" -> "we will clarify"
* fix "is referred to (for details, see [5])"

Section 3.5.
* What are 'self' and 'O' and how are they related? Maybe the authors
mean what is done later in section 4.3 and 'obj' should be used
instead of 'self', and 'O' would be I[obj]\tau. Is this correct?
Please clarify.
* The get_D function is said to be the projection from the object
universe to D_\bot. Is the object universe the set of all object
representations (oid, tag, a1, ..., an)? If so, by projection to
D_\bot, do you mean selecting the tag? If not, what is it?
* what does the superscript "(0)" in the equation for "self.a" do?
why is it absent in the equation for "self.a@pre"? 

Section 4.1.
* "the possibility to be non-existent" -> "the possibility for a value to be 
non-existent"
* In the interpretation of X+Y, the x is repeated, the second should be y 
instead of x.
* It is required that null_Boolean and true = \bot, but since the
semantic domain has been lifted twice to represent both invalid and
null, it is not clear which \bot is this, the one for null or for
invalid? Perhaps some notational aid would be useful.
* In the last paragraph: "analogously" should be "analogous". Also, I
suggest rephrasing so that you don't use the word "besides" twice.

Section 4.2.
* "isomorphic" -> "isomorphically" 
* The last paragraph on page 10 begins with "The referential strict equality
works as follows" but the "explanation" doesn't actually explain it. 
Either present the formal definition or rephrase the explanation.

Section 4.3.
* In the last paragraph it is assumed that C < B, but why? the previous 
equations do not seem to show any relation between C objects and B objects.
* "may never passed" -> "may never be passed" 

Section 4.4.
* "The semantics of this operator is defined that [...]" should be "The
semantics 
of this operator is defined such that [...]"

Section 6
* "In Figure 2 and Listing 1.1 describes a class" -> "Figure 2 and Listing 1.1 
describe a class"
* Fig 2: The color attribute is Boolean. Which is red and which is black?
* "have to be considered additionally" -> "have to be considered separately"

Section 7
* "more narrower" -> "narrower"

References
* fix capitalization in reference [7]

All sections
* The paper is one and a half pages over the limit. It must be trimmed 
substantially. Cutting that much material while preserving the quality
of the paper will be a challenge 
* A note about style: the paper uses inconsistent font styles for
different concepts like attributes and classes. Sometimes italic is
used, sometimes verbatim, sometimes normal font. There should be
better consistency.

*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*

Third reviewer's review:

Summary of the submission <<<

The paper presents a formal semantics, including null references, for parts of
OCL 2.1, as exhibited in their HOL-OCL framework.

Evaluation <<<

The paper does what it says: it highlights the (now widely accepted) confusion
between invalid and null in OCL 2.x, presents a semantics in HOL-OCL, discusses
some of the consequences, and illustrates the approach with a small example. 

The approach appears to be well thought out. The fact that there is a
tool-checked version of the theory is helpful. The paper itself is reasonably
well written (there are a number of typos or grammatically incorrect sentences)
but quite difficult to follow: I found the presentation rather terse, with very
limited (or non-existent) explanations for a non-OCL/HOL-OCL expert; the
authors would probably do well to find an alternative approach to presenting
this work at a conference than the current style, which I think does their work
a disservice.

The authors would improve their paper by discussing other implementations of
OCL that do support null and/or invalid (or equivalent constructs), as well as
similar formalisms, such as Eiffel or Alloy. In particular, exploring the
limitations of the existing Eclipse OCL compiler would be helpful and
productive. As well, better explanations for all of the
definitions/equivalences would really help. For example, on page 11, the
so-called "straightforward" definition of accessor functions takes quite a bit
of parsing to interpret.

The statement "casts on null are always valid, since they have an individual
dynamic type" is somewhat confusing: what does "they" refer to? Why might casts
on null be useful? This isn't made clear.

Overall, the paper delivers what it promises; however, the presentation is not
particularly helpful in guiding the reader through the contributions. Moreover,
the paper is well over the page limit; if the paper is accepted the authors
will probably find it difficult to cut it down to 15 pages.

*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*